$\forall$${\it ds}$:fpf(Id; $x$.Type), ${\it es}$:event\_system\{i:l\}, $i$:Id.
\\[0ex]@$i$ discrete ${\it ds}$
\\[0ex]$\Rightarrow$ ($\forall$$t$:rationals. es{-}init{-}elapsed(${\it es}$; $i$; $t$) = es{-}init{-}state(${\it es}$; $i$) $\in$ decl{-}state(${\it ds}$))